Skip to content

feat(Analysis/Convolution): add convolution_symm, convolution, (3 more lemmas)#41557

Open
lakesare wants to merge 11 commits into
leanprover-community:masterfrom
lakesare:carleson-Convolution
Open

feat(Analysis/Convolution): add convolution_symm, convolution, (3 more lemmas)#41557
lakesare wants to merge 11 commits into
leanprover-community:masterfrom
lakesare:carleson-Convolution

Conversation

@lakesare

@lakesare lakesare commented Jul 10, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Upstreaming from Carleson: /Carleson/ToMathlib/Analysis/Convolution.lean

Upstreamed theorems

  • theorem convolution_symm
    • renamed g to f' (to reuse the existing section variable)
  • theorem AEStronglyMeasurable.convolution (refactored)
  • lemma lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm (refactored)
    • removed the comment "This implies both of the following theorems convolutionExists_of_memLp_memLp and enorm_convolution_le_eLpNorm_mul_eLpNorm.", because the comment would create an impression that it's an auxiliary lemma that shouldn't be used on its own
  • theorem ConvolutionExists.of_memLp_memLp (slightly refactored)
    • (hf : AEStronglyMeasurable f μ) and (hg : AEStronglyMeasurable g μ) were removed, because we can derive those hypotheses from hfp.aestronglyMeasurable and hgq.aestronglyMeasurable respectively (which we did during refactoring)
  • theorem enorm_convolution_le_eLpNorm_mul_eLpNorm

  • lemma lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm,
    theorem ConvolutionExists.of_memLp_memLp,
    theorem enorm_convolution_le_eLpNorm_mul_eLpNorm

    • turned (hpq : p.HolderConjugate q) into an instance implicit [hpq : p.HolderConjugate q] (there does exist a class HolderConjugate for ENNReals, so mathlib seems to use instance implicits in such cases, like e.g. here)

  • theorem AEStronglyMeasurable.convolution,
    lemma lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm,
    theorem ConvolutionExists.of_memLp_memLp,
    theorem enorm_convolution_le_eLpNorm_mul_eLpNorm

@github-actions github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jul 10, 2026
@github-actions

github-actions Bot commented Jul 10, 2026

Copy link
Copy Markdown

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

@lakesare

lakesare commented Jul 10, 2026

Copy link
Copy Markdown
Contributor Author

carleson

@github-actions github-actions Bot added carleson part of the ongoing formalization of Carleson's theorem t-analysis Analysis (normed *, calculus) labels Jul 10, 2026
@github-actions

github-actions Bot commented Jul 10, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary 2c77bfe2e2

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff (regex)

+ AEStronglyMeasurable.convolution
+ ConvolutionExists.of_memLp_memLp
+ convolution_symm
+ enorm_convolution_le_eLpNorm_mul_eLpNorm
+ lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 2c77bfe).

  • +5 new declarations
  • −0 removed declarations
+MeasureTheory.AEStronglyMeasurable.convolution
+MeasureTheory.ConvolutionExists.of_memLp_memLp
+MeasureTheory.convolution_symm
+MeasureTheory.enorm_convolution_le_eLpNorm_mul_eLpNorm
+MeasureTheory.lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 2c77bfe2e2
Reference commit 87a6eccfb8

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@lakesare

lakesare commented Jul 10, 2026

Copy link
Copy Markdown
Contributor Author

WIP

@github-actions github-actions Bot added the WIP Work in progress label Jul 10, 2026
@lakesare

lakesare commented Jul 12, 2026

Copy link
Copy Markdown
Contributor Author

-WIP

@github-actions github-actions Bot removed the WIP Work in progress label Jul 12, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

carleson part of the ongoing formalization of Carleson's theorem new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@lakesare